@* A CHEX script about relations and sets.
This example of \CHEX\ is intended to follow the general definitions
in the `second \CHEX\ script'. Let's imagine that all those definitions
have already been given.

First we introduce a type called `|elt|' on which relations and sets
will be defined. Everything that follows could be made more general
by including `|elt:atom|' as the first parameter to every function,
but that would make this script unnecessary verbose.

@f set==true

@p
elt:=#:atom. {there's a special kind of |atom| called an |elt|}
rel:=(x,y:elt)bool:(x,y:elt)atom. {a relation maps a pair of |elt|s to a |bool|}

@ Various properties of relations are fundamental in mathematics. The three
most important properties are defined here: A relation might be reflexive,
symmetric, and/or transitive.

\def\?{\mathrel{\rm R}}
In the comments, we write `$x\?y$' if |r(x,y)| holds.

@p
rpred(r:rel;x:elt):=r(x,x):bool. {$x\?x$}
reflexive(r:rel):=for_all(elt,rpred(r)):bool. {$\forall x\;(x\?x)$}
use_reflexivity(x:elt;r:rel;p:proof(reflexive(r)))
 :=specialize(elt,rpred(r),x,p):proof(r(x,x)).@/
@#
spred2(r:rel;x,y:elt):=implies(r(x,y),r(y,x)):bool. {$x\?y\Rightarrow y\?x$}
spred1(r:rel;x:elt):=for_all(elt,spred2(r,x)):bool. {$\forall y\;\\{spred}(r,x,y)$}
symmetric(r:rel):=for_all(elt,spred1(r)):bool.
	{$\forall x\;\forall y\;\\{spred}(r,x,y)$}
use_symmetry(x,y:elt;r:rel;p:proof(symmetric(r));q:proof(r(x,y)))
 :=modus_ponens(r(x,y),r(y,x),
  specialize(elt,spred2(r,x),y,specialize(elt,spred1(r),x,p))):proof(r(y,x)).@/
@#
tpred3(r:rel;x,y,z:elt):=implies(and(r(x,y),r(y,z)),r(x,z)):bool.
	{$x\?y\land y\?z\Rightarrow x\?z$}
tpred2(r:rel;x,y:elt):=for_all(elt,tpred3(r,x,y)):bool. {$\forall z\ldots$}
tpred1(r:rel;x:elt):=for_all(elt,tpred2(r,x)):bool. {$\forall y\;\forall z\ldots$}
transitive(r:rel):=for_all(elt,tpred1(r)):bool.
	{$\forall x\;\forall y\;\forall z\ldots$}
use_transitivity(x,y,z:elt;r:rel;p:proof(transitive(r));
 p1:proof(r(x,y)); p2:proof(r(y,z))):=
 modus_ponens(and(r(x,y),r(y,z)),r(x,z),
  specialize(elt,tpred3(r,x,y),z,specialize(elt,tpred2(r,x),y,
    specialize(elt,tpred1(r),x,p))),
  conjunction(r(x,y),r(y,z),p1,p2)):proof(r(x,z)).

@ An equivalence relation is reflexive, symmetric, and transitive.

@p
rs_rel(r:rel):=and(reflexive(r),symmetric(r)):bool. {reflexive and symmetric}
equiv_rel(r:rel):=and(rs_rel(r),transitive(r)):bool. {and transitive too}
refl_equiv(r:rel;p:proof(equiv_rel(r))):=
 first_conjunct(reflexive(r),symmetric(r),
  first_conjunct(rs_rel(r),transitive(r),p)):proof(reflexive(r)).@#
symm_equiv(r:rel;p:proof(equiv_rel(r))):=
 second_conjunct(reflexive(r),symmetric(r),
  first_conjunct(rs_rel(r),transitive(r),p)):proof(symmetric(r)).@#
trans_equiv(r:rel;p:proof(equiv_rel(r))):=
 second_conjunct(rs_rel(r),transitive(r),p):proof(transitive(r)).

@ Next we define the notion of a set, which is sort of a one-dimensional
relation. In the comments we write `$x\in s$' if $s(x)$ holds.

@p
set:=(x:elt)bool:(x:elt)atom.@/
in(x:elt;s:set):=proof(s(x)):atom. {$\T x\in S$}

@ The most basic relation on sets is that of set inclusion, written `$\subseteq$'.

@p
incl_pred(s,t:set;x:elt):=implies(s(x),t(x)):bool. {$x\in s\Rightarrow x\in t$}
set_incl(s,t:set):=for_all(elt,incl_pred(s,t)):bool. {$\forall x\ldots$}
is_incl(s,t:set):=proof(set_incl(s,t)):atom. {$\T s\subseteq t$}
set_move(s,t:set;p:is_incl(s,t);x:elt;q:in(x,s)):=
 modus_ponens(s(x),t(x),specialize(elt,incl_pred(s,t),x,p),q):in(x,t).
	{if $x\in s$ and $s\subseteq t$ then $x\in t$}

@ Set inclusion is reflexive and transitive.

@p
set_incl_refl(s:set):=
 generalize(elt,incl_pred(s,s),(x:elt)imp_refl(s(x))):is_incl(s,s).
	{$\T s\subseteq s$}
@#
step1(s,t,u:set;p:is_incl(s,t);q:is_incl(t,u);x:elt):=
 implication(s(x),u(x),(r:in(x,s))set_move(t,u,q,x,set_move(s,t,p,x,r))):
 proof(incl_pred(s,u,x)).
	{if $x\in s$ and $s\subseteq t$ and $t\subseteq u$ then $x\in u$}
set_incl_trans(s,t,u:set;p:is_incl(s,t);q:is_incl(t,u)):=
 generalize(elt,incl_pred(s,u),step1(s,t,u,p,q)):is_incl(s,u).
	{if $s\subseteq t$ and $t\subseteq u$ then $s\subseteq u$}

@ Another basic relation on sets is the notion of set equality.

@p
set_eq(s,t:set):=and(set_incl(s,t),set_incl(t,s)):bool.
	{$s\subseteq t$ and $t\subseteq s$}
is_eq(s,t:set):=proof(set_eq(s,t)):atom.
	{$\T s=t$}

@ Set equality is reflexive, symmetric, and transitive.

@p
set_eq_refl(s:set):=
 conjunction(set_incl(s,s),set_incl(s,s),set_incl_refl(s),set_incl_refl(s)):
 is_eq(s,s).
	{$\T s=s$}
set_eq_symm(s,t:set;p:is_eq(s,t)):=
 and_symm(set_incl(s,t),set_incl(t,s),p):is_eq(t,s).
	{if $s=t$ then $t=s$}

step1(s,t,u:set;p:is_eq(s,t);q:is_eq(t,u)):=
 set_incl_trans(s,t,u,first_conjunct(set_incl(s,t),set_incl(t,s),p),
  first_conjunct(set_incl(t,u),set_incl(u,t),q)):is_incl(s,u).
	{if $s=t$ and $t=u$ then $s\subseteq u$}
step2(s,t,u:set;p:is_eq(s,t);q:is_eq(t,u)):=
 step1(u,t,s,set_eq_symm(t,u,q),set_eq_symm(s,t,p)):is_incl(u,s).
	{if $s=t$ and $t=u$ then $u\subseteq s$}
set_eq_trans(s,t,u:set;p:is_eq(s,t);q:is_eq(t,u)):=
 conjunction(set_incl(s,u),set_incl(u,s),step1(s,t,u,p,q),step2(s,t,u,p,q)):is_eq(s,u).
	{if $s=t$ and $t=u$ then $s=u$}

@ Now we will study the properties of an arbitrary equivalence relation.
For simplicity, we call it `E'. (For generality, we could have added
two parameters, `\ignorespaces
|E:rel;assumption:proof(eq_rel(E))|', to each of the
functions that follow.)

\def\?{\mathrel{\rm E}}

@p
E:=#:rel.	{E is a relation}
assumption:=#:proof(equiv_rel(E)). {E is an equivalence relation}
I(x,y:elt):=proof(E(x,y)):atom. {$\T x\?y$}
E_refl(x:elt):=use_reflexivity(x,E,refl_equiv(E,assumption)):I(x,x). {$\T x\?x$}
E_symm(x,y:elt;p:I(x,y)):=
 use_symmetry(x,y,E,symm_equiv(E,assumption),p):I(y,x).
	{if $x\?y$ then $y\?x$}
E_trans(x,y,z:elt;p:I(x,y);q:I(y,z)):=
 use_transitivity(x,y,z,E,trans_equiv(E,assumption),p,q):I(x,z).
	{if $x\?y$ and $y\?z$ then $x\?z$}

@ If |x| is an element then |E(x)| is the ``equivalence class'' of~|x|.
The rest of this script is devoted to a study of the elementary properties
of equivalence classes.

In the comments we shall write `$[x]$' for $x$'s equivalence class.
It is easy to prove that $x\in[x]$:

@p
proposition0(x:elt):=E_refl(x):in(x,E(x)).

@ Next we prove that $x\?y$ implies $[x]=[y]$.

@p
step1(x,y,z:elt;p:I(x,y);q:I(x,z)):=E_trans(y,x,z,E_symm(x,y,p),q):I(y,z).
	{if $x\?y$ and $x\?z$ then $y\?z$}
step2(x,y:elt;p:I(x,y);z:elt):=implication(E(x,z),E(y,z),step1(x,y,z,p)):
 proof(implies(E(x,z),E(y,z))).
	{if $x\?y$ then $x\?z\Rightarrow y\?z$}
lemma1(x,y:elt;p:I(x,y)):=generalize(elt,incl_pred(E(x),E(y)),step2(x,y,p)):
 is_incl(E(x),E(y)).
	{if $x\?y$ then $[x]\subseteq[y]$}
proposition1(x,y:elt;p:I(x,y)):=
 conjunction(set_incl(E(x),E(y)),set_incl(E(y),E(x)),
  lemma1(x,y,p),lemma1(y,x,E_symm(x,y,p))):
 is_eq(E(x),E(y)).
	{if $x\?y$ then $[x]=[y]$}

@ Conversely, if $[x]=[y]$, we must have $x\?y$.

@p
step1(x,y:elt;p:is_eq(E(x),E(y))):=
 first_conjunct(set_incl(E(x),E(y)),set_incl(E(y),E(x)),p):is_incl(E(x),E(y)).
	{if $[x]=[y]$ then $[x]\subseteq[y]$}
step2(x,y:elt;p:is_eq(E(x),E(y))):=
 specialize(elt,incl_pred(E(x),E(y)),x,step1(x,y,p)):
 proof(implies(E(x,x),E(y,x))).
	{if $[x]=[y]$ then $x\?x\Rightarrow y\?x$}
proposition2(x,y:elt;p:is_eq(E(x),E(y))):=
 E_symm(y,x,modus_ponens(E(x,x),E(y,x),step2(x,y,p),E_refl(x))):I(x,y).
	{if $[x]=[y]$ then $x\?y$}

@ An equivalence class is a set that equals $[x]$ for some $x$.

@p
Eclass(s:set;x:elt):=set_eq(s,E(x)):bool. {$s=[x]$}
is_Eclass(s:set):=proof(exists(elt,Eclass(s))):atom.
	{$\exists x\;(s=[x])$}

@ Each equivalence class therefore has a ``representative'' element $x$,
called its |Erep| and denoted $\hat s$.

@p
Erep(s:set;p:is_Eclass(s)):=choose(elt,Eclass(s),p):elt. {$\hat s$ is an element}
IErep(s:set;p:is_Eclass(s)):=thus(elt,Eclass(s),p):is_eq(s,E(Erep(s,p))).
	{$\T s=[\hat s]$}

@ If |s| is an equivalence class and $x\in s$, we have $x\?\hat s$.

@p
step1(s:set;p:is_Eclass(s)):=@|
 first_conjunct(set_incl(s,E(Erep(s,p))),set_incl(E(Erep(s,p)),s),IErep(s,p)):
 is_incl(s,E(Erep(s,p))). {$\T s\subseteq[\hat s]$}
proposition3(s:set;p:is_Eclass(s);x:elt;q:in(x,s)):=
 set_move(s,E(Erep(s,p)),step1(s,p),x,q):I(Erep(s,p),x).
	{if $x\in s$ then $\hat s\?x$}

@ Now we're almost ready to prove the principal theorem of these notes,
the fact that equivalence classes are either disjoint or equal.

@p
meets(s,t:set):=exists(elt,(x:elt)and(s(x),t(x))):bool.
	{$\exists x\;(x\in s\;\land\; x\in t)$}
disjoint_or_equal(s,t:set):=implies(meets(s,t),set_eq(s,t)):bool.
	{if $s$ meets $t$ then $s=t$}
@#
common_elt(s,t:set;p:proof(meets(s,t))):=
 choose(elt,(x:elt)and(s(x),t(x)),p):elt.	{if $s$ meets $t$, this is a common element}
common_first(s,t:set;p:proof(meets(s,t))):=
 first_conjunct(s(common_elt(s,t,p)),
  t(common_elt(s,t,p)),thus(elt,(x:elt)and(s(x),t(x)),p)):in(common_elt(s,t,p),s).
	{the common element is in $s$}
common_second(s,t:set;p:proof(meets(s,t))):=
 second_conjunct(s(common_elt(s,t,p)),
  t(common_elt(s,t,p)),thus(elt,(x:elt)and(s(x),t(x)),p)):in(common_elt(s,t,p),t).
	{the common element is in $t$}

@ This is it: The main theorem at last!

@p
step1(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 proposition3(s,p,common_elt(s,t,r),common_first(s,t,r)):
 I(Erep(s,p),common_elt(s,t,r)).
	{if equivalence classes $s$ and $t$ meet, their common element
		is equivalent to $\hat s$}
step2(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 proposition3(t,q,common_elt(s,t,r),common_second(s,t,r)):
 I(Erep(t,q),common_elt(s,t,r)).
	{and also equivalent to $\hat t$}
step3(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 E_trans(Erep(s,p),common_elt(s,t,r),Erep(t,q),step1(s,t,p,q,r),
  E_symm(Erep(t,q),common_elt(s,t,r),step2(s,t,p,q,r))):
 I(Erep(s,p),Erep(t,q)).
	{hence $\hat s$ is equivalent to $\hat t$}
step4(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 proposition1(Erep(s,p),Erep(t,q),step3(s,t,p,q,r)):
 is_eq(E(Erep(s,p)),E(Erep(t,q))).
	{hence $[\hat s]=[\mkern2mu\hat t\mkern2mu]$}
step5(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 IErep(s,p):is_eq(s,E(Erep(s,p))).
	{but $s=[\hat s]$}
step6(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 IErep(t,q):is_eq(t,E(Erep(t,q))).
	{and $t=[\mkern2mu\hat t\mkern2mu]$}
step7(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 set_eq_trans(s,E(Erep(s,p)),E(Erep(t,q)),step5(s,t,p,q,r),step4(s,t,p,q,r)):
 is_eq(s,E(Erep(t,q))).	{so $s=[\mkern2mu\hat t\mkern2mu]$}
step8(s,t:set;p:is_Eclass(s);q:is_Eclass(t);r:proof(meets(s,t))):=
 set_eq_trans(s,E(Erep(t,q)),t,step7(s,t,p,q,r),
  set_eq_symm(t,E(Erep(t,q)),step6(s,t,p,q,r))):
 is_eq(s,t).	{and in fact $s=t$}
proposition4(s,t:set;p:is_Eclass(s);q:is_Eclass(t)):=
 implication(meets(s,t),set_eq(s,t),step8(s,t,p,q)):
 proof(disjoint_or_equal(s,t)). {qed}